Nuprl Lemma : R-interface-compat-self
11,40
postcript
pdf
A
:es_realizer{i:l}. R-Feasible{i:l}(
A
)
R-interface-compat(
A
;
A
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
es
realizer
wf
,
R-Feasible
wf
,
R-Feasible-self-interface
,
R-self-interface-implies
origin
A:es_realizer{i:l}. R-Feasible{i:l}(A) 
R-interface-compat(A; A) A:es_realizer{i:l}. R-Feasible{i:l}(A) R-interface-compat(A; A) 
T Qx:A. B(x)